STM: dsys wf

ABS: i = j

STM: d-eq-Loc wf

STM: assert-d-eq-Loc

ABS: M(i)

STM: d-m wf

ABS: d-decl(D;i)

STM: d-decl wf

STM: d-decl-subtype

STM: mlnk wf d

ABS: D1  D2

STM: d-sub wf

STM: d-sub-self

ABS: @i: x:T initially x = v

STM: d-single-init wf

ABS: @i: only L affects x : t

STM: d-single-frame wf

ABS: @i: k affects only members of L

STM: d-single-aframe wf

ABS: @i: k sends only links in L

STM: d-single-bframe wf

ABS: @i: only members of L read x

STM: d-single-rframe wf

ABS: @i: only L sends on (l with tg)

STM: d-single-sframe wf

ABS: @i: with declarations ds:dsda:daeffect of k(v) is x := f s v

STM: d-single-effect wf

ABS: @i: with declarations ds:dsda:da k(v) sends f s v on link l

STM: d-single-sends wf

ABS: @i (with ds: ds action a:T precondition a(v) is P s v)

STM: d-single-pre wf

STM: ma-decla wf2

STM: decidable ma-decla

ABS: Feasible(D)

STM: d-feasible wf

STM: d-feasible-state

STM: d-da-atom-free

STM: d-ds-atom-free

STM: d-feasible-dec

ABS: d-chooser(D;dec)

STM: d-chooser wf

STM: d-feasible-dec2

STM: round-robin

STM: d-feasible-sched

ABS: d-world-state(D;i)

STM: d-world-state wf

ABS: stutter-state(s)

STM: stutter-state wf

ABS: next-world-state(D;i;s;k;v)

STM: next-world-state wf

STM: equal-next-world

ABS: d-partial-world(D;f;t';s)

STM: d-partial-world wf

ABS: d-comp(D;v;sched;dec)

STM: d-comp wf

STM: d-comp wf2

ABS: d-machine(i;M;dec)

STM: d-machine wf

ABS: d-world(D;v;sched;dec)

STM: d-world wf

STM: d-comp-step

ABS: d-comp-partial-world(D;v;sched;dec;t)

STM: d-comp-partial-world wf

STM: w-queue-partial

STM: better-d-comp-step

STM: d-comp-step2

STM: w-queue-nil

STM: d-msg-subtype

STM: d-decl-subtype2